%\documentclass[a4paper,10pt]{article}
\documentclass[envcountsect,envcountsame,runningheads,a4paper,orivec]{llncs} 
% \documentclass[runningheads,a4paper]{llncs}


%\usepackage[utf8]{inputenc} \usepackage{times}
\usepackage[T1]{fontenc} 
\usepackage{tgtermes}

\usepackage[english]{babel}
\usepackage{xspace}
\usepackage{float}
\usepackage{mathpartir}

\usepackage{amstext, amssymb, amsfonts, amsmath}
\usepackage{latexsym}
\usepackage{stmaryrd}
\usepackage{float}
\usepackage{graphicx}
\usepackage{enumerate}

\usepackage{color}
\usepackage{url}
\usepackage{hyperref}
\usepackage{proof}

\usepackage{macron}
\usepackage{typecasemacro}



\newenvironment{rcases}
  {\left\lbrace\begin{aligned}}
  {\end{aligned}\right\rbrace}
  
\usepackage{lineno}

\newtheorem{newnotation}[theorem]{Notation}



%opening
\title{
An Event-Based Approach to Runtime Adaptation in Communication-Centric Systems\thanks{DRAFT - Revision of \today}
%An Event-Based Approach to Runtime Adaptation in Communication-Centric Systems
%An Event-Based Architecture for Runtime Adaptation in Communication-Centric Systems
}
\titlerunning{Event-Based Adaptation in Communication-Centric Systems}
\author{Cinzia Di Giusto\inst{1} \and Jorge A. P\'{e}rez\inst{2}}
\authorrunning{Cinzia Di Giusto and Jorge A. P\'{e}rez}
\institute{%Universite d'Evry 
%Universit\'{e} de Nice Sophia-Antipolis
Univ. Nice Sophia Antipolis, CNRS, I3S, UMR 7271, Sophia Antipolis
\and
Johann Bernoulli Institute for Mathematics and Computer Science, University of Groningen}


\begin{document}

\maketitle

%\widowpenalty=0
%\clubpenalty=0


\begin{abstract}
%This paper addresses the enhancement of %process frameworks based on \emph{session types}
%frameworks for 
This paper presents a model of 
{session-based concurrency}
with mechanisms for \emph{runtime adaptation}. 
%Thus, our model allows to specify the dynamic update of the behavior of communication-centric systems.
Thus, our model allows to specify communication-centric systems 
whose session behavior can be dynamically updated at runtime.
We propose an \emph{event-based} approach: 
adaptation requests,
issued by the system itself or by its environment,
 are assimilated to events
which may trigger runtime adaptation routines.
Based on type-directed checks, these  routines 
%may depend on the current state of session protocols, 
%Such requests may , and are treated uniformly.
%Our approach enables rich forms of adaptation, 
naturally enable the reconfiguration of processes with active sessions.
%An associated 
We develop a 
 type system that ensures \emph{communication safety} 
%and consistent updates.
%is that well-typed processes enjoy both \emph{safety} 
and \emph{consistency} properties:
while the former guarantees
absence of runtime communication errors, 
the latter ensures that update actions  do not disrupt already established sessions.
\end{abstract}
%
%\section{Suggestions}
%%The abstract can be much shorter and more general.
%
%Mention the well-known work on exceptions for binary session types, and other session disciplines with buffers/queues~\cite{DBLP:journals/jfp/GayV10}.
%
%Before giving technical details, it would be very useful to give a concrete example for configurations/networks, and their evolution.
%The example could illustrate records, memories, etc.


% \linenumbers

\section{Introduction}\label{s:intro}
\noindent{\textit{\textbf{Context.}}}
Modern software
systems are built as assemblies of heterogeneous ar\-ti\-facts
which must interact following predefined protocols.
Correctness in these \emph{com\-mu\-ni\-ca\-tion-centric} systems
largely depends on ensuring that dialogues are consistent.
\emph{Session-based concurrency} is a type-based approach to
ensure conformance of dialogues to prescribed protocols:
dialogues are organized into %basic
units called \emph{sessions}; interaction patterns are abstracted as \emph{session types}~\cite{DBLP:conf/esop/HondaVK98},
against which specifications may be checked. %\looseness=-1

As communication-centric systems %typically %open, and
operate on open infrastructures,
\emph{runtime adaptation} appears as a crucial feature to ensure continued system operation.
Here we understand runtime adaptation as the dynamic modification of (the behavior of) the system in response to an exceptional event, 
such as, e.g., a varying requirement or a local failure.
These events are 
not necessarily catastrophic but are hard to predict.
As such, 
protocol conformance and
dynamic reconfiguration are intertwined concerns:
although
the specification of runtime adaptation is
not strictly tied to that of structured protocols,
steps of dynamic reconfiguration have a direct influence in a system's interactive behavior.

We are interested in integrating forms of
%We address the integration of mechanisms 
runtime adaptation
into models of %a model of
session-based concurrency.
As a first answer to this challenge, in previous work~\cite{GiustoP14short} we
extended a typed process framework 
for binary sessions
with basic constructs from the model of \emph{adaptable processes}~\cite{BGPZLMCS}.
%proposed the first integration of basic adaptation mechanisms into a session typed framework.
In this work,
with the aim of extending the applicability and expressiveness of the approach in~\cite{GiustoP14short}, 
 we propose %a framework in which
adaptation mechanisms which depend on the state of the session protocols active in a given location.
%thus enabling the specification of more fine-grained adaptation strategies.
As a distinctive feature, we advocate an \emph{event-based} approach:
by combining constructs for 
\emph{dynamic type inspection} 
and
\emph{non-blocking event detection} 
(as put forward by Kouzapas et al.~\cite{KouzapasJ13,Kouzapas12}), adaptation requests, both internal or external to the location, can be naturally assimilated to events.

%\paragraph{Our Approach, By Example.}
\paragraph{\textbf{A Motivating Example.}}
Here we consider a standard 
syntax for binary session types~\cite{DBLP:conf/esop/HondaVK98}:
$$
\begin{array}{rll}
\ST, \STT ::= & ?(T).\STT   & \text{input a value of type $T$, continue as $\STT$}\\ 
\sep &  !(T).\STT & \text{output a value of type $T$, continue as $\STT$}\\ 
       \sep & \&\{n_1{:}\ST_1 \dots  n_m{:}\ST_m \} \qquad & \text{branching (external choice)} \\
         \sep &  \oplus\{n_1{:}\ST_1 \dots  n_m{:}\ST_m \} & \text{selection (internal choice)} \\
   \sep &  \tend ~~\sep~~ \mu t.\ST  \sep t   &  \text{terminated and recursive session} 
%  \sep & \tend & \text{terminated session}
   \end{array}
$$
%As an example, 
%We 
where $T$ stands for both basic types (e.g., booleans, integers) and session types $\ST$.
Also, $n_1, \ldots, n_m$ denote \emph{labels}.
To illustrate session types, 
%and motivate our contributions using an example.
consider
%the %structured
%interaction of
a buyer \pt{B} and a seller \pt{S} which interact as follows. % the protocol given next. % following the protocol.
First, \pt{B} sends to \pt{S} the name of an item and \pt{S} replies back with its price.
Then, depending on the amount, \pt{B} either adds the item to its shopping cart or closes the transaction.
In the latter case the protocol ends.
In the former case \pt{B} must further choose a paying method. % and the transaction ends.
From \pt{B}'s perspective, this protocol may be described by
the session type $\ST = \,\,!\mathsf{item}.\,?\mathsf{amnt}.\,\ST_{\mathtt{pay}}$, where
$\mathsf{item}$ and $\mathsf{amnt}$ are base types and
%$\ST_{\mathtt{pay}}$ is %defined as
\begin{equation*}
\ST_{\mathtt{pay}} \,=\,\oplus\{\mathtt{addItem}:\, \oplus\{\mathtt{ccard}:\, \ST_\mathtt{cc} \,,\, \mathtt{payp}:\, \ST_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \}.
\end{equation*}
%In the syntax of session types,
%Above `$.$' denotes sequential composition, $!$ and $?$ stand for output and input, %respectively,
%and $\tend$ stands for the empty protocol.
Thus, 
session type $\ST$ says that protocol
 $\ST_{\mathtt{pay}}$ may only be enabled after sending a
value of type $\mathsf{item}$ and receiving a value of type $\mathsf{amnt}$.
Also,
$\mathtt{addItem}$, $\mathtt{ccard}$, $\mathtt{cc}$, and $\mathtt{payp}$ denote labels
in the internal choice.
%completed protocol. CINZIA: I think that the word completed can be misleading here
%In $\ST_{\mathtt{pay}}$,
%Session
Types
%we write
$\ST_\mathtt{cc}$ and $\ST_\mathtt{pp}$ denote the behavior of each payment method.
Following the protocol abstracted by $\ST$,
code for
\pt{B} may be specified as a $\pi$-calculus process.
Processes $P$ and $R$ below give
two specifications for \pt{B}:
\begin{eqnarray*}
P & = & \outC{x}{\mathsf{book}}.\inC{x}{a}.\ifte{a < 50}{\select{x}{\mathtt{addItem}};\select{x}{\mathtt{ccard}};P^{\mathsf{c}}}{\select{x}{\mathtt{cancel}};\mathbf{0}} \\
R & = & \outC{x}{\mathsf{game}}.\inC{x}{b}.\ifte{b < 80}{\select{x}{\mathtt{addItem}};\select{x}{\mathtt{payp}};R^{\mathsf{p}}}{\select{x}{\mathtt{cancel}};\mathbf{0}}
\end{eqnarray*}
Thus, although both $P$ and $R$ implement $\ST$,
their behavior is rather different, for they purchase different items using different payment methods (which are abstracted by processes $P^{\mathsf{c}}$ and $R^{\mathsf{p}}$).
Let us now analyze the situation for the seller $\pt{S}$.
To ensure protocol compatibility and absence of communication errors,
%$\STT$,
the session type for \pt{S}, denoted $\STT$,
should be \emph{dual} to $\ST$. This is written $\ST \cdual \STT$.
Intuitively, duality decrees that
%That is,
every action from \pt{B} must be matched by a complementary action from \pt{S}, e.g., every output of a string in $\ST$ is matched by an input of a string in $\STT$.
In our example, we let $\STT = \,\,?\mathsf{item}.\,!\mathsf{amnt}.\,\STT_{\mathtt{pay}}$, where
 $\STT_{\mathtt{pay}}$ and a process implementation for \pt{S} are as follows:
\begin{eqnarray*}
\STT_{\mathtt{pay}} & = & \&\{\mathtt{addItem}:\, \&\{\mathtt{ccard}:\, \STT_\mathtt{cc} \,,\, \mathtt{payp}:\, \STT_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \} \\
Q & = & \inC{y}{i}.\outC{y}{price(i)}.\branch{y}{\mathtt{addItem} : \branch{y}{\mathtt{ccard}: Q^{\mathtt{c}} \alte \mathtt{ppal}: Q^{\mathsf{p}}} \alte \mathtt{cancel}: \mathbf{0}}
\end{eqnarray*}
where
%$\&$ is the type for external choice, dual to $\oplus$, and 
$price$ stands for an auxiliary function. % from $\mathsf{item}$ to $\mathsf{amnt}$.
Also, %types
$\STT_{\mathtt{cc}}$ and $\STT_{\mathtt{pp}}$ are the duals of $\ST_{\mathtt{cc}}$ and $\ST_{\mathtt{pp}}$; they are realized by processes
$Q_y^{\mathsf{c}}$ and $Q_y^{\mathsf{p}}$. %, respectively.
%$\STT_{\mathtt{cc}}$ and $\STT_{\mathtt{pp}}$ (the duals of $\ST_{\mathtt{cc}}$ and $\ST_{\mathtt{pp}}$).
The interaction of $P$ and $Q$ is defined using %in session-based concurrency 
\emph{session initialization} constructs: process
$\nopenr{u}{x{:}\ST}.P$ denotes the \emph{request} of a session of type $\ST$;
dually, $\nopena{u}{x{:}\ST}.P$ denotes the \emph{acceptance} of a session of type $\ST$.
In both cases, $u$ denotes a \emph{(shared) name} used for synchronization. 
In our example, we may have 
%\begin{equation*}
\begin{eqnarray*}
Sys & = &  \nopenr{u}{x{:}\ST}.P \para \nopena{u}{y{:}\STT}.Q 
  \pired   \restr{\cha}{(P\subst{\cha^+}{x} \para Q\subst{\cha^-}{y})} = S'
\end{eqnarray*}
%\end{equation*}
Thus, upon synchronization on $u$,
a new session $\cha$ is established.
Intuitively,
in process $S'$  
session $\cha$ is ``split'' into two \emph{session channels} (or \emph{endpoints}) $\cha^+$ and $\cha^-$: we write $+$ and $-$ to
denote their opposing \emph{polarities}, which make their complementarity manifest.
The use of restriction
$\restr{\cha}$ covers both channels, thus
ensuring an interference-free medium for executing the session protocols described by $\ST$ and $\STT$.

In this work, we are interested in 
%In this context, the challenge of runtime adaptation consists in 
 ways of expressing and reasoning about the dynamic modification of session-typed processes such as $P$ and $Q$ above. 
  Such modifications may be desirable to 
  react to exceptional runtime conditions (say, an error) or to 
  implement new requirements. For instance, the type below defines a new payment method for \pt{S}:
  \begin{equation*}
\STT_{\mathtt{gift}} \,=\,\&\{\mathtt{addItem}:\, \&\{\mathtt{giftc}:\, \STT_\mathtt{gc} \,,\, \mathtt{ccard}:\, \STT_\mathtt{cc} \,,\, \mathtt{payp}:\, \STT_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \} 
\end{equation*}
Intuitively, $\STT_{\mathtt{gift}}$ \emph{extends} $\STT_{\mathtt{pay}}$ with a new alternative on label $\mathtt{giftc}$.
As such,  it is safe to use a process implementing  $\STT_{\mathtt{gift}}$  wherever a process implementing 
 $\STT_{\mathtt{pay}}$ is required.
 The \emph{safe substitution} principle that connects $\STT_{\mathtt{gift}}$  and  $\STT_{\mathtt{pay}}$ is formalized by a \emph{subtyping} relation on session types~\cite{DBLP:journals/acta/GayH05}, denoted $\csub$. 
In our example, we have $\STT_{\mathtt{pay}} \csub \STT_{\mathtt{gift}}$. 

 In previous work~\cite{GiustoP14short} we studied how to update processes when sessions have not yet been established; this suffices to analyze runtime adaptation for processes such as $Sys$ above. In this paper, we go further and address the runtime adaptation of processes such as $S'$ above, which contain already established session protocols.
As we would like to guarantee that adaptation preserves overall system correctness, 
a key challenge is ensuring that adaptation does not jeopardize such protocols. Continuing our example, let $S''$ be the process resulting from $S'$ above, after the first step stipulated by $\ST$ and $\STT$ (i.e., an exchange of a value of type $\mathsf{item}$).
Intuitively, at that point, the buyer part of $S'$ will have session type $?\mathsf{amnt}.\,\ST_{\mathtt{pay}}$, whereas the
seller part of $S'$ will have session type $!\mathsf{amnt}.\,\STT_{\mathtt{pay}}$.
Suppose we wish to modify at runtime the part of $S''$ realizing the buyer behavior.
To preserve protocol correctness,
a candidate new implementation must conform, up to $\csub$, to the type
$?\mathsf{amnt}.\,\ST_{\mathtt{pay}}$;  a process realizing
any other type will fail to safely interact with the part of $S''$  implementing the seller.
In~\cite{GiustoP14short} we defined the notion of \emph{consistency} to formalize
the correspondence between declared session protocols and the processes installed by steps of runtime adaptation.
As we will see, consistency is still appropriate 
for reasoning about runtime adaptation of processes with active sessions.

\paragraph{\textbf{Our Approach.}}
Having motivated the context of our contributions, we
move on to describe some technical details.
We rely on
a process language which extends session $\pi$-calculi with \emph{locations},
\emph{located processes}, and \emph{update processes}~\cite{BGPZLMCS}.
We use \emph{locations} as explicit delimiters for 
process behavior:
%runtime adaptation:
these are transparent, possibly nested computation sites.
Given a location $\locf{loc}$ and a process $P$,
the \emph{located process} $\scomponent{\locf{loc}}{P}$ denotes the fact that $P$ resides in \locf{loc} (or, alternatively, that $P$ has scope $\locf{loc}$).
This way, e.g.,
process
\begin{equation*}
W = \scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ \nopenr{u}{x{:}\ST}.P} \para \scomponentbig{\locf{seller}}{ \nopena{u}{y{:}\STT}.Q} \,}
\end{equation*}
represents an explicitly distributed variant of $Sys$ above:
the partners now reside in locations \locf{buyer} and \locf{seller}; location \locf{sys} encloses the whole system.
%We use locations as explicit delimiters for runtime adaptation steps:
An \emph{update process}, denoted $\nadapt{\locf{loc}}{U}$, intuitively says that the behavior currently enclosed by
\locf{loc}
should be replaced according to 
the adaptation routine
$U$.
%This way,
%to define adaptation %at the level of
%%for endpoints
%we may extend $W$ with update processes
%$\nadapt{\locf{buyer}}{R_b}$ and $\nadapt{\locf{seller}}{R_r}$.
Since a location may enclose
one or more %interacting parties,
session channels,
update processes allow for flexible specifications of adaptation routines. %than one session.
This way, e.g., one may specify an update on \locf{buyer} that does not involve \locf{seller} (and vice versa);
also, %by defining an appropriate $\nadapt{\locf{buyer}}{R_b}$;
a system-level adaptation could be defined by adding 
a process $\nadapt{\locf{sys}}{U_s}$
in parallel to $W$, 
given an $U_s$ that accounts for both buyer and seller behaviors.

The
integration of runtime adaptation into sessions %-based concurrency
is delicate, and involves
defining 
not only \emph{what} should be the  state of the system after adaptation but also 
\emph{when}
an adaptation step should be triggered. % after such a step.
To rule out careless adaptation steps which jeopardize established protocols, % (or even discard active endpoints),
communication and adaptation actions should be harmonized.
As hinted at above, in previous work~\cite{GiustoP14short}
we proposed
%a solution that consists in
admitting adaptation actions only when locations do not enclose running sessions.
%This means, e.g., that an upgrade of the payment protocols in \locf{seller} is only enabled when the seller process is idle.
%not interacting with a buyer.
This is a simple solution that 
%is \emph{asymmetric}, %in the sense that for
privileges communication over adaptation, in the sense that adaptation is enabled only
when sessions are not yet active.
Still, in realistic applications it may be
desirable to give communication and adaptation
 a similar status.
%However, it is easy to imagine actual protocols in which communication and adaptation have a similar status.
%Returning to the example,
%an % system-level
%adaptation which adds a new payment method to the seller
%(and extends the buyer's interface)
%would
%%come in handy for active
%be useful for running
%sessions in which the buyer has not yet selected how to pay.
%
To this end, in this paper we admit the adaptation of locations with running sessions.
We propose update processes
$\nadapt{\locf{loc}}{U}$ in which $U$ is able to
%with the ability of
dynamically check
the current state of the
session protocols running in \locf{loc}.
In their simplest form, our update processes
concern only one session channel and are of the shape
%are written
\begin{equation*}
{\nadaptbig{\locf{loc}}{\mycase{{x}}{{x_{}^{}{:}\STT_{}^{i}}}{U_i}{i \in I}}}
\end{equation*}
where
$I$ is a finite index set,
$x$ denotes a channel variable, 
each $\STT^i$ and $U_i$ 
denotes a session type and an 
\emph{alternative} (process) $U_i$, respectively.
(We assume $x$ occurs free in $U_i$.)
The informal semantics 
for this construct is better understood by considering 
its interaction with a
 located process
$\scomponentbig{\locf{loc}}{ Q} $
in which $Q$ implements a session of type $\ST$ along channel $\cha^p$.
%There are two possibilities for the interaction between t
The two processes may interact as follows.
If there is a  $j \in I$ such that
 types $\ST$ and $\STT^j$ ``match'' (up to $\csub$), %(roughly $\STT^j$ is a subtype of $\ST$)
then there is a reduction  to process
$\scomponentbig{\locf{loc}}{U_j\subst{\cha^p}{x}}$.
Otherwise, if no $\STT^j$ validates a match, then there is a
reduction to process
$\scomponentbig{\locf{loc}}{ Q}$, 
keeping the  behavior of \locf{loc} unchanged and consuming the update.
%i.e., the behavior of \locf{loc} is kept unchanged and the update is consumed.

In general, update processes may define adaptation for locations enclosing more than one session channel.
In the distributed buyer-seller example, %For instance,
the process below defines
a runtime update which depends on the current state of the two channels at location $\locf{sys}$:
%\begin{equation}
%R_{xy} = {\nadaptbig{\locf{sys}}{\mycase{{x,y}}{x{:}\ST^{}_{\mathtt{pay}} \,;\, y{:}\STT^{}_{\mathtt{pay}}}{\scomponent{\locf{buyer}}{ P'_x} \para \scomponent{\locf{seller}}{ Q'_y}}{}}} \label{eq:intro}
%\end{equation}
\begin{equation}
U_{xy} = {\nadaptbigg{\locf{sys}\,}{
\mathsf{case\,}x,y\, \mathsf{of}
\begin{rcases}
(x{:}\ST \,;\, y{:}\STT) & : \scomponent{\locf{buyer}}{R} \para \scomponent{\locf{seller}}{Q} \\
(x{:}\ST^{}_{\mathtt{pay}} \,;\, y{:}\STT^{}_{\mathtt{pay}}) & : \scomponent{\locf{buyer}}{ P^*} \para \scomponent{\locf{seller}}{ Q^*}
\end{rcases}
}} \label{eq:intro}
\end{equation}
%Intuitively, %
%Process
$U_{xy} $ %is an update process with only one alternative.
defines two possibilities for runtime adaptation.
%There are two possibilities for update which depend on the protocol state.
If the protocol has just been established (i.e., current types are $\ST$ and $\STT$) then only the buyer is updated---its new behavior will be given by $R$ above.
If both item and price information have been already exchanged then  implementations $P^*$ and $Q^*$, compliant with types $\ST_{\mathtt{pay}}$ and $\STT_{\mathtt{pay}}$, are installed.

Update processes rely on the protocol state at a given location to assess the suitability of adaptation routines.
%adaptation actions may safely take place on locations enclosing open sessions.
Our semantics for update relies on
(a)~\emph{monitors} which store the current type for each running session; and
(b)~a type-directed test on the monitors
%subtyping to test the state of a set of sessions
enclosed in a given location.
This test % as a %actually corresponds to
generalizes the $\mathtt{typecase}$ construct in~\cite{Kouzapas12}.

%\paragraph{\textbf{Event-Based Adaptation.}}
While expressive,
%Defined at the level of locations,
our typeful update processes %thus offer a flexible and expressive mechanism for runtime adaptation.
by themselves %, however, these processes
do not specify \emph{when} adaptation should be available.
Even though update processes could be embedded within session communication prefixes (thus creating causal dependencies between communication and adaptation),
such a specification style would only allow to handle exceptional conditions which can be fully characterized in advance.
Other kinds of exceptional conditions, in particular contextual and/or unsolicited runtime conditions, are much harder to express by interleaving update processes
within structured protocols.

%Indeed, since update processes are consumed after every test (i.e., they are not persistent), it is not clear how they should occur in specifications nor how they should be triggered.

To offer a uniform solution to this issue,
%the constructs of
we propose a \emph{event-based} approach
to trigger updates.
%In order %, we rely on \emph{events}.
We endow each location with a \emph{queue} of adaptation requests;
such requests
%these requests
%are simply treated as messages and
may be internal or external to the location.
In our example, an external request could be, e.g.,
%a signal from the infrastructure on which both partners are deployed, or
a warning message from the buyer's bank indicating that an exchange with the bank is required before committing to the purchase with the seller.

Location queues are independent from session behavior.
Their identity is visible to processes;
they are intended as interfaces with other processes and the environment.
%This way, e.g., the queue of location \locf{seller} becomes the only way in which its surrounding context may only influence the communication behavior.
To issue an adaptation request $r$ for location $\locf{loc}$, our process syntax includes \emph{adaptation signals}, written $\outC{\locf{loc}}{r}$.
%where $r$ stands for an adaptation request.
Similar to ordinary communication prefixes, 
these signals are orthogonal to sessions.
% processes such as $P_x$ and $Q_y$ may issue adaptation requests.
Then, 
we may
detect the presence of %message
request $r$ in the queue of %location
\locf{loc}
using the \emph{arrival predicate} $\arrive{\locf{loc}, r}$~\cite{Kouzapas12}.
As an example, let $\mathtt{upd}_E$ denote  an \emph{external} adaptation request.
%This way, e.g.,
%As an illustration of our event-based constructs for adaptation,
To continuously check if an external request  has been queued for
\locf{sys}, 
the process below combines process $U_{xy}$ in \eqref{eq:intro} with arrival predicates, conditionals, and recursion:
\begin{equation}
U^*_{xy} = \mu \rv{X}.\ifte{\arrive{\locf{sys}, \mathtt{upd}_E}}{U_{xy}}{\rv{X}}
\end{equation}
%Process $U^*_{xy}$ . As soon as such a request is detected update process $U_{xy}$ will be triggered.

We couple our process model for session-based concurrency and runtime adaptation with a type system
that ensures the following key properties:
\begin{enumerate}[-]
\item \emph{Safety}: well-typed programs do not exhibit communication errors (e.g., mismatched messages).
\item \emph{Consistency}: well-typed programs do not allow adaptation actions that disrupt already established sessions.
\end{enumerate}
Safety is the typical guarantee expected from any session type discipline, here considered in a richer setting that combines session communication with runtime adaptation. In contrast, consistency is a guarantee unique to our setting: it connects the behavior of the adaptation mechanisms with the preservation of prescribed typed interfaces.
We show that well-typed programs are safe and consistent (Theorem~\ref{t:safety}): this ensures that specified session protocols are respected, while forbidding incautious adaptation steps that could accidentally remove or disrupt the session behavior of interacting partners.

%\paragraph
%\noindent{\textbf{Organization.}}
\paragraph{\textbf{Organization.}}
The rest of the paper is organized as follows.
Next we present our event-based process model of session communication with typeful constructs for 
%event-based 
runtime adaptation (\S\,\ref{s:evadap}). Then, we present our
session type system, which ensures safety and consistency for processes with adaptation mechanisms (\S\,\ref{s:types}).
In \S\,\ref{s:compart} we discuss a process model of communication and adaptation 
with explicit compartments; it distills the main features of the model in \S\,\ref{s:evadap}.
At the end, we discuss related works and draw some concluding remarks 
(\S\,\ref{s:relw}).
%(\S\,\ref{s:concl}).
The appendix %collects .
gives full sets of reduction and typing rules.
The appendix collects omitted definitions and proofs.%\looseness=-1



\section{The Process Model: Syntax and Semantics}\label{s:evadap}
%ADD POINTERS TO TYPES (duality, subtyping)


\begin{table}[t!]
$$
\begin{array}{lrlr}
%u & ::=  &   x, y  \sepr a, b & \text{names}	\\
% k & ::=  &   x, y \sepr \cha^{+}, \cha^{-} & \text{channels}	\\
%d & ::= & a, b  \,\sepr \cha^{+}, \cha^{-} & \text{identifiers} \\
%v & ::= & \mathtt{true}, \mathtt{false} \sepr a, b  \sepr \cha^{+}, \cha^{-} & \text{values} \\
%r	&::= &  \mathtt{upd}_I \sepr \mathtt{upd}_E \sepr\mathtt{upg} \sepr \cdots &\text{adaptation messages} \\
e & ::= & v \sepr x, y, z  \sepr k = k \sepr a = a & \text{expressions}  \\
%  & \sepr & \arrive{u}  \sepr \arrive{k} \sepr \arrive{k,h} & \text{arrive predicates (usual)}\\ 
  & \sepr & \arrive{\locf{loc}, r} & \text{arrival predicate} \\ 
P & ::=  &   \nopenr{u}{x:\ST}.P  ~~\sepr~~ \nopena{u}{x:\ST}.P  ~~\sepr~~\close{k}.P& \text{session request / acceptance / closure}	 \\
%	& \sepr &   \nopena{u}{x:\ST}.P  & \text{session acceptance}	\vspace{0.5mm} \\
	& \sepr &  \outC{k}{e}.P ~~~~\sepr~~ \inC{k}{x}.P  & \text{data output /input } \\
  %	&\sepr &    \inC{k}{x}.P  & \text{data input} \vspace{0.5mm} \\
	&\sepr&   \select{k}{n};P ~~\sepr~~  \branch{k}{n_i{:}P_i}_{i \in I} & \text{selection / branching} \\
%    &\sepr&   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} & \text{branching} \vspace{0.5mm}\\
%		&\sepr&   \close{k}.P & \text{close session}	 \vspace{0.5mm}\\
    &\sepr&   \mu \rv{X}.P ~\,\sepr~~ \rv{X} & \text{recursion / rec. variable}  \\
%	& \sepr &   \rv{X}& \text{recursion variable}  \vspace{0.5mm}\\
  	& \sepr &   P \para  P  ~~\sepr~~   \mathbf{0}  & \text{parallel composition / inaction } \\	 
	&\sepr&   \restr{\cha}{P} ~\sepr~~ \restr{u}{P} ~\sepr~ \ifte{e}{P}{Q} & \text{channel / name hiding / conditional}	\\
%		  	& \sepr &  \ifte{e}{P}{Q} & \text{conditional} \\
%	&\sepr&   \restr{a}{P}  & \text{name hiding}	\vspace{0.5mm} \\
%	&\sepr&   \mathbf{0}  & \text{inaction} \vspace{1.5mm} \\
	&\sepr&   \que{k}{\ST}  & \text{session monitor}  \\ 
		&\sepr&  \scomponent{\locf{loc}}{P}  & \text{located process}  \\
%	&\sepr&  \nadapt{l}{P} & \text{update process}\\
	&\sepr&  \nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}} \quad& \text{typeful update process} \\
	&\sepr&   \outC{\locf{loc}}{r} \sepr \que{\locf{loc}}{\til{r}} & \text{adaptation signal / queue} %\vspace{0.5mm} \\
	%&\sepr&   \que{\locf{loc}}{\til{r}}  & \text{queue for locations} 
%p	&::= &  + \sepr - &\text{channel polarities} \\
%h	&::= &  v \sepr n &\text{messages}  
%    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \mathtt{not}(e) \sepr  \ldots & \text{expressions}
\end{array} 
$$
\caption{Process Syntax. %Session Processes with Runtime Adaptation: Syntax.
Above, annotation $\ST$ denotes a session type. % (cf. Def.~\ref{d:types})
} \label{tab:syntax}
%\vspace{-2mm}
\end{table}


%TO DO: mention abbreviations (branching), notation for labels and locations, and close process, annotations for service requests, location messages.

%Our process language of sessions with runtime adaptation
%%In a nutshell, it which 
%combines the synchronous $\pi$-calculus 
%that we have considered in~\cite{DBLP:conf/sac/GiustoP13} with constructs from the eventful session framework in~\cite{Kouzapas12}. 
%%We  also give an operational semantics for processes \\
%%, and illustrate its use with a simple example. \\

%\noindent{\bf Syntax.~}
\paragraph{\textbf{Syntax.}}
We %consider the following 
rely on 
base sets for  
\emph{names}, ranged over by $u, a, b \ldots$; 
\emph{(session) channels}, ranged over by $k, \cha^p, \ldots$, with \emph{polarity} $p \in \{+,-\}$;
\emph{labels}, ranged over by $n, n', \ldots$; 
and \emph{variables}, ranged over by $x, y, \ldots$.
\emph{Values}, ranged over $v, v', \ldots$, may include 
booleans (written $\mathtt{false}$ and $\mathtt{true}$),
integers,  names, and channels. 
We use $r$ to range over \emph{adaptation messages}: two instances are 
$\mathtt{upd}_I$ and $\mathtt{upd}_E$, for internal and external requests.
We use $\,\til{\cdot}\,$ to denote finite sequences. 
Thus, e.g., $\til{x}$ is a sequence of variables $x_1, \ldots, x_n$.
We use $\epsilon$ to denote the empty sequence.

Table~\ref{tab:syntax} reports the syntax of expressions and processes. 
Processes include usual constructs for %intra-session 
input, output, and labeled choice. 
%Communicated (\emph{delegation}).
Common forms of recursion, parallel composition, conditionals, and %name\-/\-chan\-nel 
restriction are also included.
As %hinted at above, 
illustrated in~\S\,\ref{s:intro},
constructs for session establishment %(request and accept)
are annotated with a session type $\ST$,
% and on \emph{duality}, denoted $\cdual$; see~\cite{DBLP:journals/acta/GayH05} and~\S\,\ref{s:types}.
which is useful in derived static analyses.
A prefix for closing a session, inherited from~\cite{GiustoP14short}, is convenient to structure specifications. %Also, the process syntax includes 
%Binding is as follows: 
%the channel 
Variable $x$ is bound in processes 
$\nopenr{u}{x{:}\ST}.P$, $\nopena{u}{x{:}\ST}.P$, and 
%$x$ is bound in 
$\inC{k}{x}.P$. 
Binding for name and channel restriction is as usual.
Also, recursion variable $\rv{X}$ is bound in  process $\mu \rv{X}.P$.
%Based on these intuitions, g
Given a process $P$, its sets of free/bound channels, names, variables, and recursion variables---noted 
$\mathsf{fc}(P)$, $\mathsf{fn}(P)$, $\mathsf{fv}(P)$, $\mathsf{fpv}(P)$, $\mathsf{bc}(P)$, $\mathsf{bn}(P)$, $\mathsf{bv}(P)$, and $\mathsf{bpv}(P)$, respectively---are   as expected. 
%In all cases, w
We always rely on usual notions of $\alpha$-conversion %(noted $\equiv_\alpha$) 
and (capture-avoiding) substitution, denoted 
$\subst{k}{x}$ (for channels) and $\subst{P}{\rv{X}}$ (for processes). 
We write $\subst{k_1, \ldots, k_n}{x_1, \ldots, x_n}$ to stand for an $n$-ary simultaneous substitution. 
Processes without free variables or free channels are called \emph{programs}.


Up to here, the language is a  synchronous $\pi$-calculus with sessions. 
Building upon 
\emph{locations} $\locf{loc}, \locf{l_1}, \locf{l_2}, \ldots$, 
%\emph{adaptation messages} (ranged over $r, r', \ldots$), 
constructs 
for adaptation
are:
% the following: 
%\begin{enumerate}[-]
%\item 
\emph{located processes}, denoted $\scomponent{\locf{loc}}{P}$; 
%\item 
\emph{update processes}, denoted $\nadaptbig{\locf{loc}}{\mycase{x_1, \ldots, x_m}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}$; 
%\item runtime queues for channels and locations, denoted $ \que{\cha}{\ST} $ and $ \que{\locf{loc}}{\til{r}} $, respectively; 
%\item 
\emph{(session) monitors}, denoted $ \que{\cha^p}{\ST} $; 
%\item 
\emph{location queues}, denoted $ \que{\locf{loc}}{\til{r}} $; 
and
%\item 
\emph{adaptation  signals}, denoted $\outC{\locf{loc}}{r}$.
%\item 
Moreover, expressions include the 
\emph{arrival predicate}  $\arrive{\locf{loc}, r}$.

%\end{enumerate}
%while located processes have been central in our previous works~\cite{DBLP:conf/sac/GiustoP13,BGPZLMCS}, constructs (b)--(d) above have been first introduced in~\cite{Kouzapas12}. As 
%we explain in detail next, here we adapt these constructs to the case of runtime adaptation (an issue not explored in~\cite{Kouzapas12}).
We now comment on these elements.
%As in~\cite{DBLP:conf/sac/GiustoP13,BGPZLMCS}, given a process $P$ and a location $\locf{loc}$, 
%process $\scomponent{\locf{loc}}{P}$ denotes a \emph{located process}.
%Locations are transparent: inside \locf{loc}, process $P$ can freely evolve, possibly interacting with its environment. 
%They can be nested, which is particularly convenient when structuring processes for adaptability purposes.
\emph{Located processes} and 
\emph{update processes}
have been motivated in~\S\,\ref{s:intro}.
Here we just remark that 
update processes
are assumed to refer to at least one variable $x_i$ and to offer at least one alternative $Q_i$.
Also, variables $x_1, \ldots, x_m$ are bound in 
 $\nadaptbig{\locf{loc}}{\mycase{x_1, \ldots, x_m}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}$; this process
is often abbreviated as 
$\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}$.
% variables $x_i$ are bound in $\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}$.
Update processes 
%the latter 
%\emph{Eventful update processes} rely on the current state of the session protocols running within a given location in order to determine an appropriate adaptation routine. For the sake of clarity, we illustrate first the particular case of \emph{diadic} eventful update processes (i.e., useful to adapt locations with at most two active sessions); then, we discuss the general $n$-adic case. 
%A diadic eventful update process is written as follows:
%\begin{equation}\label{eq:dya}
%\nadaptbig{\locf{loc}}{\mycase{x_1, x_2}{{x_{1}^{}{:}\ST_{1}^{i} \,;\,  x_{2}^{}{:}\ST_{2}^{i}}}{Q_i}{i \in {I}}}
%\end{equation}
%%Process~\eqref{eq:dya} 
%and 
%represents an adaptation routine for  sessions %$\cha_1^p, \cha_2^q$ located  at 
%enclosed by $\locf{loc}$. 
%As formalized by the operational semantics (see below),
%this process works  as a case operator on the session protocols currently associated to any channels $\cha_1^p, \cha_2^q$ in \locf{loc}:
%if such protocols ``match'' with one of the $\ST^j_1, \ST^j_2$ in the update process, then 
%the current behavior at \locf{loc} will be replaced with process $Q_j$.
%Otherwise, if no such match is possible, then the behavior at \locf{loc} is left unchanged and the update process at \locf{loc} is consumed. 
%Notice that a diadic update process  will be able to update \emph{at most} two sessions established at \locf{loc}. 
%This way, e.g., an update process such as~\eqref{eq:dya} could be defined to match only one session (say $\cha_1^p$). 
%%This way, for instance, if the current behavior at \locf{loc} involves exactly one running session, and the update process offers an alternative $Q_j$ which requires only a single matching option, then runtime adaptation will be possible.
%The general case for eventful update processes (given in (b) above) %is  in Table~\ref{tab:syntax}. It 
%generalizes \eqref{eq:dya} by 
%handling runtime adaptation for locations with at most $n$ running sessions.
%%\begin{equation}
%%\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}
%%\end{equation}
%Note that each option $i \in I$ may refer to a subset of the variables declared as $\til{x}$.
%Eventful update processes 
 generalize the $\mathtt{typecase}$ introduced in~\cite{Kouzapas12}, which defines a case-like choice based on a single channel;
 in contrast,  
 to specify adaptation for locations with multiple open sessions, 
 our update processes define type-directed checks over one or more channels.
%Note that we use dynamic session type inspection only for runtime adaptation purposes, while 
%in~\cite{Kouzapas12} 
%$\mathtt{typecase}$ is part of the syntax of processes. 
%This choice enables us 
%%to focus on  the key aspects of event-based concurrency that are key to runtime adaptation. Also, it allows us 
%%the limited use of our generalized form of $\mathtt{typecase}$ is also useful 
%to retain a standard session type syntax; see~\S\,\ref{s:types}. %simplify some parts of our technical development.

Update processes go hand-in-hand with \emph{monitors}, 
runtime entities which keep the current protocol state  at a given channel. 
We write $\que{\cha^p}{\ST}$ to denote the monitor which stores the protocol state $\ST$ for 
channel $\cha^p$. 
In~\cite{Kouzapas12}, a similar construct is used to store in-transit messages in  asynchronous communication. 
For simplicity, 
%and to highlight the adaptation mechanisms of our language, 
here we consider synchronous communication; monitors store only the current protocol state. This choice is aligned with our goal of identifying the core elements from the eventful session framework that are central in defining runtime adaptation (cf. Remark~\ref{rem:asynch}).
%\looseness=-1
%DA TOGLIERE: Extensions of our framework to the asynchronous case are discussed in Remark X.

\emph{Location queues}, not present in~\cite{Kouzapas12}, 
%are associated to locations; they 
handle adaptation requests, modeled as a possibly empty sequence of messages $\til{r}$.
%they are denoted $\que{\locf{loc}}{\til{r}}$.
Location queues 
%They
enable us to give a unified treatment to adaptation requests, internal and external. 
%The empty queue is denoted $\que{\locf{loc}}{\epsilon}$.
Given $\que{\locf{loc}}{\til{r}}$, it is worth observing that messages $\til{r}$ are not related to communication as abstracted by session types. This represents the fact that we handle adaptation requests and structured session exchanges as orthogonal issues. 
An \emph{adaptation signal} $\outC{\locf{loc}}{r}$ enqueues request $r$ into the location queue of $\locf{loc}$.
To this end, as detailed below, the operational semantics defines synchronizations between adaptation signals and location queues.
%
To connect  runtime adaptation and communication, our language allows the coupling of update processes with the \emph{arrival predicate on locations}, denoted \arrive{\locf{loc}, r}. %, which we now explain.
Inspired by the $\mathtt{arrive}$ predicate in~\cite{Kouzapas12}, this predicate detects if a  message $r$ 
%(which may represent a request for adaptation or upgrade) 
has been placed in the queue of  \locf{loc}. 

%Summing up, o
Our  language embodies several concerns related to runtime adaptation: using adaptation signals and location queues 
we may formally express
%\emph{who} may specify/trigger an adaptation event; by using queues  it also decrees 
\emph{how} an adaptation request is issued; arrival predicates enable us to specify \emph{when} adaptation will be handled; using update processes and monitors we may specify \emph{what} is the goal of an adaptation event. 



%, noted $\sub{\widetilde{c}}{\widetilde{x}}$ (for data), $\sub{\kappa^p}{{x}}$ (for channels), and $\sub{P}{\mathsf{X}}$ (for processes).


\begin{table}[h!]
\[
\begin{array}{lc}
 \rulename{r:Open} & 
\locc{\nopena{u}{x:\ST}.P} \para  \locd{\nopenr{u}{y:\STT}.Q} \pired \hfill  \\
& \hfill 
\restr{\cha}{\big({\locc{P\sub{\cha^{p}}{x} \para \que{\cha^p}{\ST}}  \para  \locd{Q\sub{\cha^{\overline{p}}}{y} \para \que{\cha^{\overline{p}}}{\STT} }\big) } \quad (\ST \cdual \STT) \vspace{1.5mm} \\

\rulename{r:Com} &
\locc{\outCn{\overline{\cha}^{\,p}}{v}.P \para \que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\STT}}} 
\pired \hfill \\
&\hfill
\locc{P \para \que{\cha^p}{\ST}} \para  \locd{Q\sub{{v}\,}{{x}} \para \que{\cha^{\overline{p}}}{\STT} } 
%\quad (\ST \cdual \STT) %\quad ({e} \downarrow {c}) 
\vspace{1.5mm}
\\
%\rulename{r:Sel} &
%C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \para  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}} \} \para \\
%& D\{\select{\cha^{\,\overline{p}}}{n_j};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\overline{\ST_j} \}_{j \in J}}  \} 
%\pired \\
%& 
%\hfill C\{P_j \para \que{\cha^p}{\ST_j} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\overline{\ST_j}} \}  \quad (1 \leq j \leq m)  
\rulename{r:Sel} &
\locc{\branch{\cha^{\,p}}{n_j{:}P_j}_{j \in J}\! \para\!  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}}}\! \para \!
\locd{\select{\cha^{\,\overline{p}}}{n_i};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\STT_j \}_{j \in J}} } \\
& \hfill \pired   C\{P_i \para \que{\cha^p}{\ST_i} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\STT_i} \}  
\quad (%\ST_i \cdual \STT_i,\, 
i \in J)  
\vspace{1.5mm}
\\
\rulename{r:Clo} &
\locc{\close{\cha^{\,p}}.P \para \que{\cha^p}{\tend} } \para  \locd{\close{\cha^{\,\overline{p}}}.Q \para \que{\cha^{\overline{p}}}{\tend}} \pired %\\
%& \hfill 
\locc{P} \para  \locd{Q} \vspace{ 2mm}
\\
\rulename{r:Eva} & \text{if }e \pired e' \text{ then } \evc{E}[e] \pired \evc{E}[e']
\vspace{1.5mm}\\
 \rulename{r:Par} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{1.5mm}
\\
%\rulename{r:Con} &  \text{if }P \pired P' \text{ then } \locc{P} \pired \locc{P'}
%\vspace{1.5mm}\\
%  \rulename{r:Loc} &
% \text{if } P \pired P'~~\text{then}~~ \scomponent{l}{P} \pired \scomponent{l}{P'} \vspace{1.5mm}
% \\ 
\rulename{r:ResN} & \text{if }P \pired P' \text{ then } (\nu a)P \pired (\nu a)P'
\vspace{1.5mm}\\
\rulename{r:ResC} &\text{if }P \pired P' \text{ then } (\nu \cha)P \pired (\nu \cha)P'
\vspace{1.5mm}\\
 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{1.5mm}
\\
 \rulename{r:Rec} &
\recu\,\rv X. P \pired P\subst{\recu\,\rv X. P }{\rv X}
\vspace{1.5mm}\\
\rulename{r:IfTrue} &
\ifte{\mathtt{true}}{P}{Q} \pired P    \vspace{1.5mm}
\\
 \rulename{r:IfFalse} &
\ifte{\mathtt{false}}{P}{Q} \pired Q   \vspace{1.5mm}\\
\rulename{r:UReq} &  \locc{\que{\locf{loc}}{\til{r}_1}} \para \locd{\outC{\locf{loc}}{r}} \pired 
\locc{\que{\locf{loc}}{\til{r}_1 \cdot r}} \para \locd{\mathbf{0}}
\vspace{2mm}\\
\rulename{r:Arr1} & 
\displaystyle\frac{ \til{r} =  r_1 \cdot \til{r_0} }{
\locc{\evc{E}[\arrive{\locf{loc},r_1}]} \para \locd{\que{\locf{loc}}{\til{r}}} \pired \locc{\evc{E}[\mathtt{true}]}
\para \locd{\que{\locf{loc}}{\til{r_0}}} }  
\vspace{2mm}\\
\rulename{r:Arr2} & \displaystyle\frac{ (\til{r} = r_2 \cdot \til{r_0}  \land r_1 \neq r_2) \lor \til{r} = \epsilon}{
\locc{\evc{E}[\arrive{\locf{loc},r_1}]} \para \locd{\que{\locf{loc}}{\til{r}}} \pired \locc{\evc{E}[\mathtt{false}]}
\para \locd{\que{\locf{loc}}{\til{r}}} }  
\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\rulename{r:UpdOld} & 
%\displaystyle\frac{
%\begin{array}{rcl} 
%\multicolumn{3}{c}{\mathsf{fc}(P)  = \cha_1^p, \ldots, \cha^p_n }
%%& &
%%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} 
%\\
% (V = P \land R' = R) & \bigvee  & \big(
% \mathsf{match}_I(l,\, \til{\cha},\, \til{x} ,\,  \til{x}_0 ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I},\, \{Q_i\}_{i \in I}) ~ \land~
%\\ 
%&& ~~~ V = Q_l\subst{\til{\cha}\,}{\,\til{x}_0} ~\land~
%R' = \que{\cha^p_1}{\STT_{1}^l} \para\! \cdots\! \para \que{\cha^p_n}{\STT^{l}_n} 
%  \big)
%\end{array}
%}{
%\begin{array}{l}
%\locc{\scomponent{\locf{loc}}{P \para R}} \para
%\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}   
%\pired \qquad \\
%\hfill \locc{\scomponent{\locf{loc}}{V \para R'}} \para \locd{\mathbf{0}}
%\end{array}
%} 
%\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{r:Upd} & 
\displaystyle\frac{
\begin{array}{rcl} 
\multicolumn{3}{c}{\mathsf{fc}(P) = \{ \cha_1^p, \ldots, \cha^p_m \} \qquad \forall j \in [1,..,m]. (\Pin{P}{\que{\cha^p_j}{\ST_j}})}
%& &
%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} 
\\
 (V = P) & \bigvee  & \exists l.\big(
 \mathsf{match}_I(l,\, \{\ST_1, \ldots, \ST_m\} ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}) ~ \land~
\\ 
&& \qquad V = Q_{l\,}\subst{\cha^p_1, \ldots, \cha^p_m\,}{\,x_1, \ldots, x_m} 
  \big)
\end{array}
}{
\begin{array}{l}
\locc{\scomponent{\locf{loc}}{P}} \para
\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}   
\pired \qquad \quad  \\
\hfill \locc{\scomponent{\locf{loc}}{V}} \para \locd{\mathbf{0}}
\end{array}
} 
\end{array}
%\vspace{-3mm}
\]
\caption{Reduction Semantics: Full Set of Rules.
Above, $\ST$ and $\STT$ denote session types. % (cf. Def.~\ref{d:types})
\label{tab:redsem-full}}
%\vspace{-7mm}
\end{table}

\paragraph{\textbf{Semantics.}}
The semantics of our language is given by a \emph{reduction semantics},
the smallest relation generated by the rules 
in Table~\ref{tab:redsem-full}.
We write $P \pired P'$ for the reduction from $P$ to $P'$.
Reduction relies on 
%an evaluation relation on expressions, denoted $e \downarrow v$ (where $v$ is a value). Also, it uses 
a standard notion of structural congruence, denoted~$\equiv$ (see~Appendix \ref{app:types}). %. (TO BE ADDED)
It also relies on  \emph{evaluation} and \emph{location} contexts:
\begin{eqnarray*}
\evc{E}  ::=  - \sepr \outC{k}{\evc{-}}.P \sepr  \ifte{\evc{-}}{P}{Q} \qquad \quad
C,D  ::=  - \sepr \scomponent{\locf{loc}}{C \para P}
\end{eqnarray*}
Given 
$\locc{\!\!-\!\!}$
 (resp. $\evc{E}[-]$), we write $\locc{P}$ (resp. $\evc{E}[e]$) to denote 
the process (resp. expression) obtained by filling in occurrences of hole $-$
in $C$ with $P$ (resp. in $\evc{E}$ with~$e$). 
%The extension of $\equiv$ to contexts is as expected.

We comment on the reduction rules below. 
The first four rules formalize session behavior within hierarchies of nested locations.
Using duality for session types, denoted $\cdual$ (see~\cite{DBLP:journals/acta/GayH05} and~\S\,\ref{s:types}),
in rule~\rulename{r:Open} the synchronization on a name $u$ %with dual session types 
leads to establish a session on fresh channels $\cha^p$ and $\cha^{\overline{p}}$;
also, two  monitors with the declared session types are created.
Duality for polarities $p$ is as expected: $\overline{+} = -$ and  $\overline{-} = +$.
Monitors are \emph{local} by construction: they are created in the same contexts in which the session is established. 
Rule~\rulename{r:Com} represents  communication of a value: we require both complementary prefixes and that the monitors support input and output actions. After reduction, prefixes in processes and monitors are consumed.  
Similarly, rule~\rulename{r:Sel} for labeled choice is standard, augmented with monitors. %, which should support branching and selection. 
Rule~\rulename{r:Clo} formalizes  session termination, discarding involved monitors.
The monitors in these three rules allow us to track the evolution of active session protocols. 
%It is worth observing that we require that session queues are \emph{local} to the process. This way, for instance, a process 
%\begin{equation}
%\locc{\outCn{\overline{\cha}^{\,p}}{v}.P} \para \loccp{\que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\overline{\ST}}} \nonumber
%\end{equation}
%is not able to reduce for the queue $ \cha^p$ is not local to the process executing that session.

The remaining rules in Table~\ref{tab:redsem-full} 
define our event-based approach to runtime adaptation. 
Rule~\rulename{r:UReq} treats the issue of an adaptation request $r$ as a synchronization between a location queue and an adaptation signal. The queue and the signal may be in different  contexts;  this enables ``remote'' requests. Rules~\rulename{r:Arr1} and \rulename{r:Arr2} resolve arrival predicates %within evaluation contexts
by querying the (possibly remote) queue $\til{r}$. 
Rule~\rulename{r:Upd} defines the typeful update of the current protocol state at \locf{loc}, which is given 
by an indexed set of open sessions with their associated monitors.
%While at a first sight it may appear complex, the rule actually enforces a simple case operation over the running sessions at location \locf{loc}. The rule attempts to match (via subtyping, noted  $\csub$ in~\S\,\ref{s:types}) the current protocol state at \locf{loc} (embodied by the open sessions $\til{\cha}$ and their associated queues $R$) with the different options offered by the update process. The rule focuses on finding the first positive match; if no such 
%match exists then the current behavior at \locf{loc} ($P$, in the rule) is left unchanged, and the update process is consumed.\looseness=-1 
The rule attempts to match such protocol state with the first suitable option offered by an update process for \locf{loc}.
If there is no matching alternative the current protocol state at \locf{loc} is kept unchanged. %, and the update process is consumed.
By an abuse of notation, we write
$\Pin{P}{P_1}$ 
to indicate that $P_1$ occurs in $P$, i.e., 
if $P = C[P_1]$ for some  $C$.
Formally, 
given an index set $I$ over the update process, 
suitability with respect to the behavior at \locf{loc}
is defined 
by predicate $\mathsf{match}_I$ in Definition~\ref{d:matchp} below. 
Using subtyping $\csub$ (see~\cite{DBLP:journals/acta/GayH05} and \S\,\ref{s:types}), the predicate holds for an $l \in I$ which 
defines a new protocol state.

%\begin{definition}[Matching (Old)]\label{d:matchp}
%Given an index set $I$, session channels $\til{\cha}$, sets of variables $\til{x}$ and $\til{x}_0$,
%an indexed sequence of session types $\{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}$, 
%an indexed set of processes $\{Q_i\}_{i \in I}$, 
%and an  $l \in I$,
%we write 
%\begin{equation}
%\mathsf{match}_I(l,\, \til{\cha},\, \til{x} ,\,  \til{x}_0 ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I},\, \{Q_i\}_{i \in I}) \nonumber
%\end{equation}
%if and only if all of the following hold:
%\begin{enumerate}[(a)]
%\item $\til{x}_0 \subseteq \til{x} \land %\til{x}_0 = \{x_1, \ldots, x_g\} \land \til{\cha} = \{\cha^p_1, \ldots, \cha^p_n\} \land 
%|\til{x}_0| = |\til{\cha}| = n \land n \leq m$
%\item $\exists I' \subseteq I.(\forall h \in I'. \mathsf{fc}(Q_h) = \til{x}_0 \land l \in I')$
%\item $\forall r < l.\exists j \in [1..n].\exists s \in [1..n].~~\STT^{r}_s \not\csub \ST_j
%~~\land~~\forall j \in [1..n].\forall s \in [1..n].~~ \STT^{l}_s \csub \ST_j $
%\end{enumerate}
%\end{definition}
%Hence,  $\til{x}_0$ denotes a set of variables of the same cardinality of $\til{\cha}$ (condition (a)).
%Using $\til{x}_0$, condition (b) singles out the subset $I'$ of $I$ of suitable candidates for adaptation routines; index $l$ must be in $I'$. Condition (c) formalizes the fact that index $l$ refers to the first alternative to match, up to subtyping. 

In addition, our  semantics includes 
standard and/or self-explanatory treatments for
reduction under evaluation contexts, parallel composition, located context, and restriction.
Also, it accounts for applications of structural congruence, recursion and conditionals.
%(with omitted rule~\rulename{r:IfFalse} being as expected).\looseness=-1 


\begin{definition}[Matching]\label{d:matchp}
Given an index set $I$, 
session types $\ST_1, \ldots, \ST_m$, 
an indexed sequence of session types $\{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}$, 
and an  $l \in I$,
we write 
\begin{equation*}
\mathsf{match}_I(l,\, \{\ST_1, \ldots, \ST_m\} ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}) 
\end{equation*}
if and only if $\forall n < l.(\exists j \in [1..m].~\STT^{n}_j \not\csub \ST_j)
\land (\bigwedge_{h \in [1..m]} \STT^{l}_h \csub \ST_h)$.
\end{definition}
%Hence,  the matching predicate formalizes the fact that index $l$ refers to the first alternative that matches,  up to subtyping. 

%\noindent{\bf Example.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\input{example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{example}
Recall process $W$ given in the Introduction. 
%\begin{equation}
%W  =   \scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ \nopenr{u}{x{:}\ST}.P^{50}} \para  \scomponentbig{\locf{seller}}{ \nopena{u}{y{:}\STT}.Q}\,} \nonumber
%\end{equation}
According to our semantics: % we have:
\begin{eqnarray*}
W & \pired& \restr{\cha}{\big(\scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ P\subst{\cha^p}{x} \para \que{\cha^p}{\ST}} \para  \scomponentbig{\locf{seller}}{Q\subst{\cha^{\overline{p}}}{y} \para \que{\cha^{\overline{p}}}{\STT}}\,} \big)}  \\ 
& \pired^2 & \restr{\cha}{\big(\scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ P' \para \que{\cha^p}{\ST_{\mathtt{pay}}}} \para  \scomponentbig{\locf{seller}}{Q' \para \que{\cha^{\overline{p}}}{\STT_{\mathtt{pay}}}}\,} \big)} 
\end{eqnarray*}
Suppose that following an external request the seller must offer a new payment method. (a gift card).
Precisely, we would like \pt{S} to act according to the   type
$\STT_{\mathtt{gift}}$ given in \S\ref{s:intro}.
%\begin{equation*}
%\STT_{\mathtt{gift}} \,=\,\&\{\mathtt{addItem}:\, \&\{\mathtt{giftc}:\, \STT_\mathtt{gc} \,,\, \mathtt{ccard}:\, \STT_\mathtt{cc} \,,\, \mathtt{payp}:\, \STT_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \} 
%\end{equation*}
Let $\ST_{\mathtt{gift}}$ be the dual of $\STT_{\mathtt{gift}}$.
We then may define the following update process $R^1_{xy}$:
\begin{equation*}
{\nadaptbig{\locf{sys}}{\mycase{{x,y}}{x{:}\ST^{}_{\mathtt{pay}} \,;\, y{:}\STT^{}_{\mathtt{pay}}}{\scomponentbig{\locf{buyer}}{ P' \para \que{x}{\ST_{\mathtt{gift}}}} \para  \scomponentbig{\locf{seller}}{Q'' \para \que{y}{\STT_{\mathtt{gift}}}}}{}}} 
\end{equation*}
Thus, $R^1_{xy}$ keeps the expected implementation for the buyer ($P'$), but updates its associated monitor.
For the seller, both the implementation and monitor are updated; above, $Q''$ stands for a process offering the three payment methods.
We may then specify the whole system as:
%\begin{equation}
$W \para \mu \rv{X}.\ifte{\arrive{\locf{sys}, \mathtt{upd}_E}}{R^1_{xy}}{\rv{X}}$.  
The type system introduced next  ensures, among other things, that updates such as $R^1_{xy}$ consider both a process and its associated monitors, ruling out the possibility of discarding the monitors that enable reduction. 
\end{example}

\section{Session Types for Eventful Runtime Adaptation}\label{s:types}
This section introduces a session type system for the process language of \S\,\ref{s:evadap}.
Our main result (Theorem~\ref{t:safety}) is that well-typed programs enjoy both \emph{safety} (absence of runtime communication errors)
and \emph{consistency} properties (update actions do not disrupt established sessions).
Our development follows the lines of the typed framework in~\cite{GiustoP14short}. 
%\begin{definition}[Types]\label{d:types}
%The syntax of \emph{basic types} (ranged over by $\capab, \sigma,   \ldots$) 
%and \emph{session types} (ranged over by $\ST, \STT, \ldots$)
%is given below. We use $T, S, \ldots$ to range over $\capab, \ST$.
%\[
%\begin{array}{lclr}
%%T, S&::=& \capab, \ST \\
%\capab, \sigma & ::= & \mathsf{name} \sepr \mathsf{bool}  ~~~& \text{basic types}\\
%
%\ST, \STT &::=  &  !(\capab).\ST \sepr ?(\capab).\ST  \sepr !(\STT).\ST \sepr ?(\STT).\ST  \quad& \text{send, receive, throw, catch} \vspace{0.5mm}\\ 
%		& \sepr &  \&\{n_1{:}\ST_1 \dots  n_m{:}\ST_m \} \sepr \oplus\{n_1{:}\ST_1 \dots  n_m{:}\ST_m \}  &  \text{branch, select} \vspace{0.5mm} \\
%		& \sepr &  \tend \!\!\!\!\!\!& \text{closed session} \vspace{0.5mm} \\
%    & \sepr  & t \sepr  \mu t.\ST & \text{type variable, recursion} 
%\end{array}
%\] %}
%\end{definition}
%\noindent 

The syntax of session types (ranged over by $\ST, \STT, \ldots$) has been already presented in the Introduction.
We consider \emph{basic types} (ranged over by $\capab, \sigma,   \ldots$) and
write $T, S, \ldots$ to range over $\capab, \ST$.
Therefore, although our process language copes with runtime adaptation, 
our type syntax is standard and retains the intuitive meaning of session types~\cite{DBLP:conf/esop/HondaVK98}, which we now briefly recall.
Type $?({\capab}).\ST$ (resp. $?(\STT).\ST$) abstracts the behavior of a channel 
which receives %a boolean or a name 
a value of type $\capab$
(resp. a channel of type $\STT$) 
and then continues as $\ST$. 
Dually, type $!({\capab}).\ST$ (resp. $!(\STT).\ST$) represents the behavior
of a channel which sends 
a value of type $\capab$
%a value (resp. a channel) 
 and then continues as $\ST$.
Type $\&\{n_1:\ST_1 \dots  n_m:\ST_m \}$ describes a branching behavior:
it offers $m$ behaviors, and if the $j$-th alternative is selected then it behaves as described by type $\ST_j$ ($1 \leq j \leq m$).
In turn, type $\oplus\{n_1:\ST_1 \dots  n_m:\ST_m \}$ describes the behavior of a channel which 
may select a single behavior among  $\ST_1, \ldots, \ST_m$ and then continues as $\ST_j$.
We use $\tend$ to type a channel with no communication behavior. Type $\mu t.\ST$ describes recursive behavior;  
as usual, we consider recursive types under equi-recursive and contractive assumptions.

Along the paper we have informally appealed to \emph{duality}  and \emph{subtyping}  over session types (denoted \cdual and \csub, resp.). 
For the sake of space, we omit their full definitions; 
we just remark that since our session type structure is standard, 
we may rely on the (coinductive) definitions given by Gay and Hole~\cite{DBLP:journals/acta/GayH05}, which are standard and well-understood.
%The extension of $\csub$ to typings $\ActS$ % ,  written $\ActS \csub \ActS'$, 
%is as expected.

%The former relies on a \emph{duality relation}; % (cf. Def.~\ref{def:dualr} in~\cite{GiustoP14ext};
%the latter uses the  notion of \emph{type simulation}. % (given by Def.~\ref{def:simul} in).
%For the sake of space, we refer to~\cite{GiustoP14ext} for full definitions of these two notions.
%
%\begin{definition}\label{d:subt} Let $T, S$ be types.
%%\begin{enumerate}[$-$]
%%\item 
%The \emph{coinductive duality relation}, denoted \cdual, is defined by $T \cdual S$ if and only if there exists a duality relation $\mcc{R}$
%such that $(T, S) \in \mcc{R}$. 
%%\item 
%The \emph{coinductive subtyping relation}, denoted \csub, is defined by $T \csub S$ if and only if there exists a type simulation $\mcc{S}$
%such that $(T, S) \in \mcc{S}$. \\
%The extension of $\csub$ to typings,  written $\ActS \csub \ActS'$, 
%arises as expected.
%%\end{enumerate}
%\end{definition}




Our typing judgments generalize usual notions with an  \emph{interface}~$\INT$.
Based on the syntactic occurrences of session establishment prefixes $\nopenr{a}{x{:}\ST}$, and $\nopena{a}{x{:}\ST}$,
the interface of a process describes the %(possibly persistent) 
services appearing in it.
We 
annotate services with a 
\emph{qualification} $\qua$, which may be `$\qual$' (linear) or `$\quau$' (unrestricted).
Thus, %intuitively, 
the interface of a process gives an ``upper bound'' on the services that it  may execute.
The typing system uses interfaces to control the behavior contained by locations after an update.
We have:


\begin{definition}[Interfaces]\label{d:interf}
We define an \emph{interface} as the multiset whose underlying set of elements  is
$\mathrm{I} = \{ \qua\,u{:}\ST ~|~ \qua \in \{\qual, \quau\}\}$ (i.e., a set of  
assignments from names to qualified session types).
%More precisely: $\mathrm{I} = \{ \qua\,u{:}\ST ~|~ \qua \in \{\qual, \quau\}\}$, 
%\text{$u$ is a name, and $\ST$ is a session type}\}$$
We use $\INT, \INT', \ldots$ to range over interfaces.
We write $dom(\INT)$ to denote the set $\{u \mid u:\ST_\qua \in \INT \}$ and  $\#_\INT(a) = h$ to mean that  $a$ occurs $h$ times in $\INT$. 
\end{definition}
%Thus, several occurrences of the same service declaration are captured by the multiset nature of interfaces.
The union of two interfaces %$\INT_1$ and $\INT_2$ 
is essentially the union of their underlying multisets.
We sometimes write $\INT \addelta a:\ST_\qual$ 
and  $\INT \addelta a:\ST_\quau$
to stand 
for $\INT \addelta\{\qual\,a{:}\ST\}$ and 
$\INT \addelta \{\quau\,a{:}\ST\}$, respectively.
Moreover, we write $\INT_\qual$ (resp. $\INT_\quau$) to denote the subset of $\INT$ involving
only assignments qualified with $\qual$ (resp. $\quau$). 
We now define an ordering relation over interfaces, relying on subtyping:

%Next definition, extends the  subtyping relation to interfaces..

\begin{definition}[Interface Ordering] \label{d:rintpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr \INT'$ iff 
\begin{enumerate}[1.]
\item $\forall (\qual\,a{:}\ST)$ such that  
 $\#_{\INT_\qual}(\qual\,a{:}\ST) = h$  with $h > 0$,
then  one of the following holds:
\begin{enumerate}[(a)]
\item there exist $h$ distinct elements $(\qual\,a{:}\STT_i) \in \INT'_\qual$ such that 
 $\ST \csub \STT_i$ for $ i \in [1..h]$;
\item there exists $(\quau\,a{:}\STT) \in \INT'_\quau$ such that  $\ST \csub \STT$.
\end{enumerate}
\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then $ (\quau \, a{:}\STT) \in \INT'_\quau $ and $\ST \csub \STT$, for some $\STT$.
\end{enumerate}


\end{definition}


%\subsection{Environments, Judgments and Typing Rules}
% \begin{table}[t]
% \textsc{Environments}
% $$
% \begin{array}{lclr}
% 		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
% \ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  k:\que{}{\ST}  & \text{typing with active sessions} \vspace{0.5mm} \\
% \Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST}_\qua \rangle \quad& \text{first-order environment} \vspace{0.5mm} \\
% \Theta &::= &  \emptyset \sepr  \Theta,\rv{X}:\type{\ActS}{\INT} \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
% \end{array}
% $$  
% \caption{Types and Typing Environments. Interfaces $\INT$ are formally introduced in Definition~\ref{d:interf}.}\label{tab:types}
% \end{table}
% 

\begin{table}[t]
\[
\begin{array}{c}

\inferrule*[right=\rulename{t:LocEnv}]{ }{\typing{\Theta, \locf{loc}:\INT}{\locf{loc}}{\INT}} 
\quad \infer[\rulename{t:Que}]
 {\judgebis{\env{\Gamma}{\Theta}}{\que{k}{\ST}}{\type{k:\que{}{\ST}}{\emptyset}}}{}
\vspace{1.5mm} \\

\infer[\rulename{t:msg}]
{\typing{\Gamma}{r_1}{\msg}}{} \qquad

\infer[\rulename{t:locQ}]
{\typing{\Gamma}{r_1;\til{r}}{\msg}}
{\typing{\Gamma}{\til{r}}{\msg} & \typing{\Gamma}{r_1}{\msg}}\vspace{1.5mm} \\

\infer[\rulename{t:arrive}]
{\judgebis{\env{\Gamma}{\Theta}}{\arrive{\locf{loc}, r}}{\bool}}
{\typing{\Theta}{\locf{loc}}{\INT} \qquad\typing{\Gamma}{r}{\msg}} 
\qquad 
\infer[\rulename{t:Sig}]
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\locf{loc}}{r}}{\type{\emptyset}{\emptyset}}}
{\typing{\Gamma}{r}{\msg}}
\vspace{1.5mm} \\


\inferrule*[right=\rulename{t:Loc} ]
 {
       \typing{\Theta}{\locf{loc}}{\INT} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } }  \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{\locf{loc}}{}{\INT}{P} }{ \type{\ActS}{\INT' }}}
 \qquad
 \infer[\rulename{t:QLoc}]
{\judgebis{\env{\Gamma}{\Theta}}{\que{\locf{loc}}{\til{r}}}{\type{\emptyset}{\emptyset}}}
{ \typing{\Gamma}{\til{r}}{\msg}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Accept}]
{\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qual , {\STT}_\qual  \rangle} \quad \gamma \csub \ST \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma}{\,\INT}}}{  \judgebis{\env{\Gamma}{\Theta}}{\nopena{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: \gamma_\qual}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Request}]
 {\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qua , {\STT}_\qual \rangle} \quad \gamma \csub \STT \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma }{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{ \nopenr{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: {\gamma}_\qual }}} 
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Clo}]
 {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \quad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\tend}{ \INT}}}
\quad
\inferrule*[right=\rulename{t:Par}]
 {
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \quad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
\vspace{2mm} \\
\infer[\rulename{t:Adapt}]
{\judgebis{\env{\Gamma}{\Theta}}{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{j}; \cdots ;x_{m}^{}{:}\STT_{m}^{j}}}{Q_j}{j \in J}}}{\type{\emptyset}{\emptyset}}}
{
%\begin{array}{c}
\typing{\Theta}{\locf{loc}}{\INT} \qquad \forall j \in J, \ \mathsf{fv}(Q_j) \setminus \{x_1, \ldots, x_m\} = \emptyset \\
\judgebis{\env{\Gamma}{\Theta}}{Q_j}{\type{x_{1}{:}\mon{\STT_{1}^{j}}; \cdots ;x_{m}{:}\mon{\STT_{m}^{j}}}{\INT_j} }  \qquad \INT_j \intpr \INT
%\end{array}
}
% \text{ where } \typeque{x:\STT} \text{ stands for } x:\STT, x:\que{}{\STT}
\vspace{2mm} \\
%\infer[\rulename{t:RVar}]{\Gamma; \Theta,\rv X: \ActS, \INT \vdash \rv X:\type{\ActS}{\INT}}{}
%\qquad
%\infer[\rulename{t:Rec} ]{\judgebis{\env{\Gamma}{\Theta}}{\mu \rv X. P}{\type{\Delta}{\INT }}} 
%{\judgebis{\env{\Gamma}{\Theta,\rv X: \type{\ActS}{\INT}}}{P}{\type{\Delta}{ \INT}} }
%\vspace{1.5mm} \\
  \infer[\rulename{t:CRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^p:\mon{\ST_1}, \cha^{\overline{p}}:\mon{\ST_2} }{ \INT}} & \ST_1 \cdual \ST_2} 
\vspace{1.5mm} \\
\infer[\!\!\rulename{t:sub} ]{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS'}{\INT'}} } 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{ \INT}}& \ActS \csub \ActS' & \INT \intpr \INT'}
~~~
 \infer[\!\!\rulename{t:NRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{u}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS }{ \INT \cup \INT_u}} \quad  \ u \notin \dom{\INT} }
% \vspace{1.5mm} \\
% \infer[\rulename{t:NRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{u}{P}}{\type{\ActS}{ \INT}}}
% {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS }{ \INT \cup \INT_u}} \quad  \ u \notin \dom{\INT} }
 %\text{ where } \INT_u \text{ contains only declarations for } u \ (i.e. \forall v\neq u, v\notin \dom{\INT_u} )
 \end{array}
 \]
\caption{Well-Typed Processes: Selected Rules.} \label{tab:ts}
%\vspace{-8mm}
\end{table}

\noindent 
We now define our typing environments. % on which our type system relies.
We write $\qua$ to range over 
qualifiers
$\qual$ and $\quau$. 
\[
\begin{array}{lclr}
%		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  k:\que{}{\ST}  & \text{typing with active sessions} \vspace{0.5mm} \\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, u:\langle \ST_\qua , \STT_\qua \rangle \quad& \text{first-order environment (with $\ST_\qua \cdual \STT_\qua$)} \vspace{0.5mm} \\
\Theta &::= &  \emptyset \sepr  \Theta,\rv{X}:\type{\ActS}{\INT} \sepr \Theta,\locf{loc}:\INT     \quad& \text{higher-order environment}
\end{array}
\]  
We consider typings $\ActS$ and environments $\Gamma$ and $\Theta$. 
Typing $\ActS$  collects
assignments from channels to session types; it describes
currently active sessions. 
In our system, 
$\ActS$ also includes \emph{bracketed assignments}, denoted $\kappa^p:\que{}{\ST}$,
which represent the type for monitors. 
Subtyping extends to these assignments ($\que{}{\ST} \csub \que{}{\STT}$ if  $\ST \csub \STT$) 
and thus to typings.
We write $dom(\ActS)$ to denote the set $\{ k^p \mid k^p:\ST \in \ActS \lor k^p:\que{}{\ST} \in \ActS\}$. 
We write $\ActS , k:\ST $  where $k \not\in dom(\ActS)$.
Furthermore, we 
write $\ActS, k:\mon{\ST}$ to 
abbreviate $\ActS, k:\ST, k:\que{}{\ST}$.
That is, $k:\mon{\ST}$  describes both a session and its associated monitor.
%The extension of $\csub$ to typings $\ActS$ is as expected.


$\Gamma$ is a first-order environment which maps expressions to basic types
and names to pairs of qualified session types.
As motivated earlier, a session type is qualified with 
`$\quau$' if it is associated to a unrestricted/persistent service; otherwise, it is qualified with 
`$\qual$'. 
The higher-order environment $\Theta$ 
collects assignments of typings to process variables and interfaces to locations.
While the former concerns recursive processes, the latter concerns located processes.
As we explain next, by relying on the combination of these two pieces of information the type system ensures that
runtime adaptation actions preserve the behavioral interfaces of a process.
We write $vdom(\Theta)= \{ \mathsf{X} \mid \mathsf{X}:\INT \in \Theta \}$ to denote the variables in the domain of $\Theta$.
Given these environments, a \emph{type judgment} is  of form \looseness=-1
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$$
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface 
$\INT$.
Selected typing rules are shown in Table~\ref{tab:ts};  
%(remaining rules can be found in~\cite{GiustoP14ext}).
remaining rules can be found in Table~\ref{t:addtyperules} (Appendix~\ref{ap:adtyping}).
Below we comment on some  of the rules in Table~\ref{tab:ts}: the rest are standard and/or self explanatory.
Rule \rulename{t:Adapt} types update processes. Notice that the typing rule  ensures that each process $Q_i$ has exactly the same active sessions that those declared in the respective case.   
Also, we require that alternatives contain both processes and monitors. 
With
$\INT_j \intpr \INT$ we guarantee that the process behavior does not ``exceed'' the expected behavior within the location.
Rule~\rulename{t:sub} takes care of  subtyping both for typings $\ActS$ and interfaces. Rule~\rulename{t:CRes} types channel restriction that ensures typing duality among partners of a session and their respective queues.
Typing of queues is given by rule \rulename{t:Que} that simply assigns  type $k:\que{}{\ST}$ to queue $\que{k}{\ST}$.
Finally, rule \rulename{t:NRes} types hiding of service names, by simply removing their declarations from the interface $\INT$ of the process.
In the rule, 
$\INT_u$ contains only declarations for $u$, i.e., $\forall v\neq u, v\notin \dom{\INT_u}$.

\looseness=-1


Our type system enjoys the standard \emph{subject reduction} property. 
We rely on \emph{balanced} typings: $\ActS$ is balanced iff 
for all $\kappa^p:\ST \in \ActS$ (resp. $\kappa^p:\que{}{\ST} \in \ActS$)
then also 
$\kappa^{\overline{p}}: \STT \in \ActS$ (resp. $\kappa^{\overline{p}}: \que{}{\STT} \in \ActS$), with $\ST \cdual \STT$.
The proof
%detailed in~\cite{GiustoP14ext}, 
detailed in the Appendix, 
proceeds by induction on the last rule applied in the reduction; it adapts the one given in \cite{GiustoP14short}.

\begin{theorem}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
\end{theorem}

We now define and state \emph{safety} and \emph{consistency} properties. 
While safety  guarantees  adherence to prescribed session types and absence of runtime errors, consistency 
%is unique to our framework with runtime adaptation and
ensures that sessions are not jeopardized by 
careless
%incautious 
 runtime adaptation actions.
Defining both properties requires the following notions of \emph{$\kappa$-processes}, \emph{$\kappa$-redexes}, 
and \emph{error process}.

\begin{definition}[$\kappa$-processes, $\kappa$-redexes, errors]\label{d:kred}
A process $P$ is a \emph{$\kappa$-process} if it is a prefixed process with subject $\kappa^p$, i.e., 
$P$ is one of the following:
\[
\inC{\kappa^{\,p}}{x}.P'  \qquad \outCn{\overline{\kappa}^{\,p}}{v}.P' \qquad      \close{\kappa^{\,p}}.P' \qquad \branch{\kappa^{\,p}}{n_i{:}P_i}_{i \in I}  \qquad   \select{\kappa^{\,p}}{n}.P'
%\begin{array}{lclcl}
%    \inC{\kappa^{\,p}}{x}.P' & \qquad &  \outCn{\overline{\kappa}^{\,p}}{v}.P' & \qquad &     \close{\kappa^{\,p}}.P'    \\
%   \branch{\kappa^{\,p}}{n_i{:}P_i}_{i \in I}  &  \quad&   \select{\kappa^{\,p}}{n}.P'  & \quad& 
%\end{array}
\]
Process $P$ is a \emph{$\kappa$-redex} if 
it contains the composition of exactly two $\kappa$-processes with opposing polarities.
$P$ is an \emph{error} if
$P \equiv (\nu \til{\kappa})(Q \para R)$
where, for some $\kappa$, $Q$ contains 
\underline{either} 
exactly 
two $\kappa$-processes that do not form a $\kappa$-redex
\underline{or}
three or more $\kappa$-processes.
\end{definition}


Informally, a process $P$
is called \emph{consistent} 
if whenever  it has a $\kappa$-redex  then  update actions do not destroy such a redex.  Below, we formalize this intuition. 
Let us write $P \pired_{\text{upd}} P'$ 
for any reduction inferred using rule $\rulename{r:Upd}$. We then define:

\begin{definition}[Safety, Consistency]\label{d:consis}
Let $P$ be a process.
We say $P$ is \emph{safe} if it never reduces into an error. 
We say $P$ is \emph{update-consistent} 
if and only if,
 for all $P'$ and $\kappa$ 
such that $P \pired^{*} P'$ and $P'$ contains a $\kappa$-redex, 
if $P' \pired_{\text{upd}} P''$
then $P''$ contains a $\kappa$-redex.
\end{definition}


We now state our main result; it follows as a  consequence of Theorem~\ref{th:subred}.
 
\begin{theorem}[Typing Ensures Safety and Consistency]\label{t:safety}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced
then program $P$ is update consistent and %never reduces into an error.
safe.
\end{theorem}

\begin{remark}[Asynchronous Communication]\label{rem:asynch}
We have focused on \emph{synchronous} communication: this allows us to give a compact semantics, relying on a standard type structure.
% in which our novel adaptation mechanisms can be cleanly presented. 
To account for asynchrony, we would require 
a runtime syntax for programs with 
queues for in-transit messages (values, sessions, labels). %; such queues would become part of the runtime syntax of programs. 
The type system must be extended to accommodate these new runtime processes. 
In our case, an extension with asynchrony  
would rely on the machinery defined in~\cite{Kouzapas12}.
\end{remark}
%\input{types.tex}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



%Another difference is that in~\cite{DBLP:conf/aplas/AndersonR12} update actions are independent from the program's syntax.

%\section{Concluding Remarks}\label{s:concl}

\newcommand{\myapp}[4]{#1\big\langle #2 \,;\, #3\,;\, #4\big\rangle }
\newcommand{\stpar}{\diamond}
\newcommand{\appar}{\parallel}
\newcommand{\mapar}{\circ}

%As discussed  in \S\,\ref{s:evadap}, 
%the novel mechanisms for runtime adaptation present in our process language operate at the level of locations.
%The introduction of located processes and mechanisms for runtime adaptation defined over locations 
%We now address the following 
%This raises a 
%natural question: 

%\noindent{\textbf{Discussion: A Compartmentalized Model of  Communication and Adaptation.}} 
%\paragraph{\textbf{Discussion: A Compartmentalized Model of  Communication and Adaptation.}} 
\section{Discussion: A Compartmentalized Model of  Communication and Adaptation}\label{s:compart} 
Giv\-en that 
the process model in \S\,\ref{s:evadap}
enables the interplay of communication and adaptation, 
how can we organize specifications to 
reflect a desirable separation of concerns?
%achieve modular treatment of runtime adaptation? 
In ongoing work, 
with the aim of specifying systems at a high-level of abstraction,
we have developed a model which defines \emph{compartments} to
isolate communication behavior and adaptation routines. 
Here we briefly describe this model, which is 
given in Table~\ref{t:model}.\looseness=-1

In a nutshell, programs of \S\,\ref{s:evadap} are now organized into \emph{systems}. A system $G$
is the composition of a set  of \emph{applications} $A_1, \ldots, A_n$ each comprising three   elements: 
a \emph{behavior} $R$, a \emph{state} $\mathsf{S}$, and a \emph{manager} $\mathcal{M}$. 
As a simple example of a system, we may consider the operating system of a smartphone, which is meant to manage a number of applications that may interact among them.
%In fact, a
Applications in our model can communicate between each other %(as in the interaction of different apps) 
or exhibit intra-application communication. %(as in an app with several modules). 
The behavior $R$ is specified as a process; 
we distinguish between located processes representing service definitions  
from located processes which make use of such definitions. % (the latter are denoted $\scomponentbig{\locf{loc}}{P^{-}}$ in Table~\ref{t:model}).
A reduction semantics (omitted) ensures that locations enclosing service definitions do not contain open (active) sessions. 
This may be convenient for defining adaptation strategies, since updates to service definitions may now be performed without concerns of disruption of active sessions. 
The state $\mathsf{S}$ collects
session monitors and location queues and it is kept separate from $R$.  
As a simple example, the buyer-seller scenario given in \S\,\ref{s:intro} 
can be casted in our model as 
\[
 \myapp{\mathsf{byr}}{\scomponentbig{\locf{buyer}}{\,  \nopenr{u@\mathsf{slr}}{x:\ST}.P}}{\mathsf{S_b}}{\mathcal{M}_b} \appar
\myapp{\mathsf{slr}}{\scomponentbig{\locf{seller}}{ \repopen{u}{y{:}\STT}.Q}}{\mathsf{S_s}}{\mathcal{M}_s} 
\]
That is, buyer   and seller  are implemented as  separate applications, named $\mathsf{byr}$  and $\mathsf{slr}$, respectively.
Above, we have $\mathsf{S_b} = \que{\locf{buyer}}{\epsilon}$   and 
$\mathsf{S_s} = \que{\locf{seller}}{\epsilon}$.

%In the smartphone scenario, the state roughly corresponds to the set of buffers available for each app.
While the manager $\mathcal{M}$
implements adaptation  at the application (local) level,
a \emph{handler} $\mathcal{H}$ defines adaptation at the 
system (global) level.
As we wish to describe communication behavior separately from adaptation routines, 
update processes are confined to handlers and managers.
A manager is  meant to react upon the arrival of an internal adaptation message $\mathtt{upd}_I$. 
As in~\S\,\ref{s:evadap},
managers may act upon the issue of an internal update request $\mathtt{upd}_I$ for some location, whereas handlers may act upon the arrival of an external update request or an application upgrade request (denoted $\mathtt{upd}_E$ and $\mathtt{upg}$, respectively).
A handler  may either  $\mathtt{upd}$ate 
or  $\mathtt{upg}$rade
the behavior at some location $\locf{loc}$ within application $a$; this is written $\locf{loc}@a$.
Upgrades are
denoted $\nupgbig{\locf{l}_1}{P}$; they are a particular form of update 
intended for service definitions only. 
In Table~\ref{t:model} we write $\ast\ift{e}{P}$ and $\repopen{u}{x{:}\ST}.P$ as shorthands for persistent conditionals and services, respectively.
\begin{table}[!t]
\begin{eqnarray*}
G & ::= & A \sepr \mathcal{H} \sepr \restr{\cha}{A} \sepr G_1 \appar G_2 \sepr \mathbf{0} \qquad \quad
A  :: =  \myapp{a}{R}{\mathsf{S}}{\mathcal{M}} \\
%g & :: = & \arrive{\locf{l}@a, \mathtt{upd}_E} \sepr g_1 \land g_2 \sepr g_1 \lor g_2\\
\mathcal{H} & ::= & 
*\,\ift{\arrive{\locf{l}_1@a, \mathtt{upd}_E}}{\nadaptbig{\locf{l}_1}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}} \\
& \sepr & *\,\ift{\arrive{\locf{l}_1@a, \mathtt{upg}}}{\nupgbig{\locf{l}_1}{P}} 
\\
R & ::= & \scomponentbig{\locf{loc}}{\nopena{u}{x{:}\ST}.P}   \sepr  \scomponentbig{\locf{loc}}{\repopen{u}{x{:}\ST}.P}   \sepr \scomponentbig{\locf{loc}}{P^{-}}  \sepr R_1 \para R_2 \\
\mathsf{S} & ::= & \que{\cha^p}{\ST} \sepr \que{\locf{loc}}{\til{r}} %\sepr \que{a}{\til{r}}  
\sepr \mathsf{S}_1 \stpar \mathsf{S}_2 \sepr \mathbf{0} \\
\mathcal{M} & ::= & *\,\ift{\arrive{\locf{l}_1, \mathtt{upd}_I}}{\nadaptbig{\locf{l}_1}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}} \sepr  \mathcal{M}_1 \mapar \mathcal{M}_2   \sepr \mathbf{0}
%& \sepr & \mathcal{M}_1 \para \mathcal{M}_2 
\end{eqnarray*}
%\vspace{-3mm}
\caption{A Compartmentalized Model of Communicating Systems: Syntax.\label{t:model}}
%\vspace{-7mm}
\end{table}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% 
% Next we briefly present some highlights of our model, which is 
% given by the syntax in Table~\ref{t:model}.
% \begin{enumerate}[-]
% \item A \emph{system} $G$
% is defined as the composition of \emph{applications} $A_1, \ldots, A_n$.
% Applications comprise three   elements: 
% a \emph{behavior} $R$, a \emph{state} $\mathsf{S}$, and a \emph{manager} $\mathcal{M}$. 
% 
% \item 
% $R$ concerns communication (session) behaviors. % processes.
% We consider a standard session $\pi$-calculus only extended with the (possibly remote) adaptation request $\outC{\locf{loc}@a}{r}$, which refers to location \locf{loc} in application $a$.
% Similarly, our notation for session requests refers to a service $u$ at application $a$.
% We write $\ast\ift{e}{P}$ and $\repopen{u}{x{:}\ST}.P$ as shorthands for persistent conditionals and services, respectively.
% Also, we write $P^{-}$ to denote the sublanguage of processes without service definitions $\nopena{u}{x{:}\ST}.P$.
% 
% 
% 
% \item $\mathsf{S}$ collects
% session monitors and location queues.  We use $\mathsf{S}_1 \stpar \mathsf{S}_2$ to denote the composition of $\mathsf{S}_1$ and $\mathsf{S}_2$.
% %contains located service definitions and invocations, the second stores monitors and location queues associated to the behavior of the application, together with a queue for the application. 
% 
% \item $\mathcal{M}$ %denoted $\mathcal{M}_1, \mathcal{M}_2,  \ldots $, 
% implements adaptation  at the application (local) level. %This scheme thus realizes the desired separation of concerns.
% As we wish to isolate communication behavior from adaptation routines, 
% update processes are confined to handlers and managers.
% A manager is  meant to react upon the arrival of an internal adaptation message $\mathtt{upd}_I$. 
%  We write 
%  $\mathcal{M}_1 \mapar \mathcal{M}_2$ 
%  to denote the composition of  $\mathcal{M}_1$ and $\mathcal{M}_2$.
% %In fact, it is worth noticing that managers may act upon the issue of an internal update request $\mathtt{upd}_I$ for some location, whereas handlers may act upon the arrival of an external update request or an application upgrade request (denoted $\mathtt{upd}_E$ and $\mathtt{upg}$, respectively).
% 
% 
% \item There are  \emph{handler} processes, denoted $\mathcal{H}_1, \mathcal{H}_2,  \ldots $, 
% which are responsible for adaptation at the 
% system (global) level.  A handler  may either  $\mathtt{upd}$ate 
% or  $\mathtt{upg}$rade
% the behavior at some location $\locf{loc}$ within application $a$; this is written $\locf{loc}@a$.
% Upgrades are
% denoted $\nupgbig{\locf{l}_1}{P}$; they are a particular form of update 
% intended for service definitions only. 
% 
% 
% 
% \item As before, locations are transparent; for simplicity, here we rule out their nesting. 
% %A design criteria in the specification of $R$ is the 
% We distinguish between located processes representing service definitions 
% from located processes which make use of such definitions.
% A reduction semantics (omitted) ensures that locations enclosing service definitions do not contain open (active) sessions. 
% This may be convenient for organizing adaptation strategies, since updates to service definitions may now be performed without concerns of disruption of active sessions. 
% 
% 
% %As it will be clear later on, this is useful to isolate service definitions. 
% 
% \end{enumerate}
% 
% 
% \begin{table}[!t]
% \begin{eqnarray*}
% G & ::= & A \sepr \mathcal{H} \sepr \restr{\cha}{A} \sepr G_1 \appar G_2 \sepr \mathbf{0} \qquad \quad
% A  :: =  \myapp{a}{R}{\mathsf{S}}{\mathcal{M}} \\
% %g & :: = & \arrive{\locf{l}@a, \mathtt{upd}_E} \sepr g_1 \land g_2 \sepr g_1 \lor g_2\\
% \mathcal{H} & ::= & 
% *\,\ift{\arrive{\locf{l}_1@a, \mathtt{upd}_E}}{\nadaptbig{\locf{l}_1}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}} \\
% & \sepr & *\,\ift{\arrive{\locf{l}_1@a, \mathtt{upg}}}{\nupgbig{\locf{l}_1}{P}} 
% \\
% R & ::= & \scomponentbig{\locf{loc}}{\nopena{u}{x{:}\ST}.P}   \sepr  \scomponentbig{\locf{loc}}{\repopen{u}{x{:}\ST}.P}   \sepr \scomponentbig{\locf{loc}}{P^{-}}  \sepr R_1 \para R_2 \\
% \mathsf{S} & ::= & \que{\cha^p}{\ST} \sepr \que{\locf{loc}}{\til{r}} %\sepr \que{a}{\til{r}}  
% \sepr \mathsf{S}_1 \stpar \mathsf{S}_2 \sepr \mathbf{0} \\
% \mathcal{M} & ::= & *\,\ift{\arrive{\locf{l}_1, \mathtt{upd}_I}}{\nadaptbig{\locf{l}_1}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}} \sepr  \mathcal{M}_1 \mapar \mathcal{M}_2   \sepr \mathbf{0}
% %& \sepr & \mathcal{M}_1 \para \mathcal{M}_2 
% \end{eqnarray*}
% %\vspace{-3mm}
% \caption{A Compartmentalized Model of Communicating Systems: Syntax\label{t:model}}
% \vspace{-8mm}
% \end{table}
% 
% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Our compartmentalized model induces specifications in %of interacting systems in 
which   communication, runtime adaptation, and state (as in, e.g., asynchronous communication) are jointly expressed, while keeping a desirable separation of concerns.
%It is worth noticing that 
Notice that
the differences between %the syntax and semantics of 
``plain'' processes 
(as given in \S\,\ref{s:evadap}) and %those for 
systems (as defined in Table~\ref{t:model}) are mostly conceptual, rather than technical. 
In fact, the higher level of abstraction that is enforced by our model does not result in additional technicalities.
%Although our compartmentalized model builds upon processes, w
We conjecture that a reduction-preserving translation of application-based specifications into processes does not exist---a main difficulty being, unsurprisingly, properly representing the separation between behavior and state. 
This difference in terms of expressiveness does not appear to affect the type system. 
%In fact, w
In future work we plan to extend the 
%We are confident that the 
typing discipline in \S\,\ref{s:types} (and its associated safety and consistency guarantees) to systems. 
%We plan to address this conjecture in future work.
%For instance, typing the upgrades is simple using interfaces


\section{Related Work and Concluding Remarks}\label{s:relw}
%\noindent\emph{\textbf{Related Work.}~}
%The closest related work is the PhD thesis of Kouzapas~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}, which introduces event-bases processes for asynchronous communication together with a complete framework to test arrival of messages and test types of queues. As mentioned throughout the paper we have been inspired by this machinery but we have considerably changed the domain and scope of application. 
% 
\paragraph{\textbf{Related Work.}}
The combination of static typing and type-directed tests for dynamic reconfiguration is not new.
For instance, 
Seco and Caires~\cite{DBLP:conf/esop/SecoC06} study this combination for a calculus for object-oriented component programming.
To the best of our knowledge, ours is the first work to develop this combination for a session process language.
As already discussed, % along the paper, %the most related works are 
we build upon constructs proposed 
in~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}. The earliest works on eventful sessions, covering theory and implementation issues, are~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11}. %; an associated journal paper is~\cite{KouzapasJ13}. %We have often referred to 
Kouzapas's PhD thesis~\cite{Kouzapas12} provides a  unified presentation of the eventful framework, with case studies including  event selectors (a building block in event-driven systems) and transformations between multithreaded and event-driven programs.  
%Besides the eventful process constructs, 
At the level of types, 
the work in~\cite{Kouzapas12} introduces session set types to support the $\mathtt{typecase}$ construct. 
%Since our typecase construct is embedded inside update processes, our type system may rely on a standard session type syntax.
We use dynamic session type inspection only for runtime adaptation;  %, while 
in~\cite{Kouzapas12} 
$\mathtt{typecase}$ is part of the process syntax. 
This choice enables us 
to retain a standard session type syntax. %; see~\S\,\ref{s:types}. 
%As mentioned above, r
Runtime adaptation of session typed processes---the main contribution of this paper---seems to be an  application of  eventful session types not previously identified.

Previous works on runtime adaptation for  session types (binary and multiparty) include~\cite{GiustoP14short,DBLP:conf/aplas/AndersonR12,CDV14}.
We have already commented on how our current approach  enhances that in our previous work~\cite{GiustoP14short}.
Both~\cite{DBLP:conf/aplas/AndersonR12} and \cite{CDV14} study adaptation for multiparty communications, which already sets a substantial difference with respect to our work. 
In~\cite{CDV14}, a set of monitors which govern the behavior of participants are derived from a global specification. Self-adaptation for monitored processes is triggered by an external adaptation function, which is often left unspecified. 
As in our work, the operational semantics for adaptation in~\cite{CDV14} uses (local) types and monitors; 
key differences include the use of type-directed checks for selecting adaptation routines that preserve consistency, and 
the use of events and queues to
handle adaptation requests.
The work~\cite{DBLP:conf/aplas/AndersonR12} studies dynamic update for message passing programs; a form of consistency for updates over threads is ensured using multiparty session types, following an asynchronous 
 communication discipline. 




\paragraph{\textbf{Concluding Remarks.}} 
%\noindent\emph{\textbf{Concluding Remarks.}~} 
%\section{Concluding Remarks}\label{s:concl}
Building upon~\cite{Kouzapas12}, 
we have introduced an eventful approach to runtime adaptation of session typed processes. 
We identified the strictly necessary eventful process constructs that enhance and refine known
mechanisms for runtime adaptation. 
Adaptation requests, both internal and external, are handled via event detectors and queues associated to locations. 
%This eventful approach to adaptation 
Our approach
enables us to 
specify rich forms of updates on locations with running sessions; this represents a concrete improvement with respect to previous works~\cite{GiustoP14short}. %, in which updates are only allowed when locations do not enclose running sessions.
We notice that expressing both internal and external exceptional events is useful in practice; 
for instance, both kinds of events coexist in  
%the Business Process Model \& Notation (BPMN) 
BPMN 2.0~(see, e.g.,~\cite[Chap.4]{DBLP:books/daglib/0031128}).
To rule out update steps that jeopardize running session protocols, 
we also introduced a type system that ensures communication safety and update consistency for session programs.
%To further motivate   our  framework, 
We have also outlined 
a high-level  model of structured interaction which 
organizes  communication and adaptation components into a sensible structure. 

Adaptation in our framework is ``monotonic'' or ``incremental'' in that changes always preserve/extend active session protocols, exploiting subtyping for enhanced flexibility.
Interestingly, our framework can be modified so that arbitrary protocols are installed
as a result of an update. One needs to 
 ensure that the endpoints of a session are present in the same location: 
 arbitrary  updates are safe as long as both endpoints %(two, in our binary case)
 are simultaneously updated with dual protocols.
% modify the operational semantics and the typing rules to
To relax our framework in this way, 
we would need to modify definitions for session matching (Def.~\ref{d:matchp}) and interface ordering (Def.~\ref{d:rintpre}).




In future work, we plan to further validate the constructs in our framework by 
%We would like %We plan to use %the eventful constructs proposed here 
%our framework
revisiting the model of \emph{supervision trees} (a mechanism for fault-tolerance in Erlang)
that we gave in~\cite{DBLP:journals/corr/GiustoP13}.
% we gave a model of supervision trees which relied on the adaptation mechanisms put forward in our previous work~\cite{GiustoP14short}).
%Our developments are kept purposefully simple, and admit several extensions. 
%% two of them are 
%%, thus, believe that by slightly modifying the present proposal  we can adapt our framework to i) describe 
%For instance, an extension with
%\emph{asynchronous} communication 
%could be obtained as discussed in Remark~\ref{rem:asynch}. 
%Also, it could be useful to explore an extension with \emph{higher-order} runtime adaptation, in which 
%location queues are refined in such a way that 
%in addition to an adaptation signal, they also receive from the environment a process defining an adaptation routine.
%In the first case, the framework proposed by Kouzapas et al. can be adopted here by simply enriching the information on channel  queues.  The second enhancement can be obtained for instance by allowing location queues to receive together with the adaptation signal an update routine to be executed on the locality. 
%Also, %well-formed systems %of the compartmentalized model % approach can be followed for architectures where states and managers 
%our process semantics
%could be %refined so as to handle also faults and communication problems. This can be achieved 
%enhanced with memories, % storing %not only the current state but also 
%%some previous history, % (as in~\cite{DBLP:journals/corr/TiezziY14}), 
%thus  allowing  
%a session to \emph{rollback} to a previous state. 
Other interesting topics 
for further development
%that we plan to address is 
include accounting for 
\emph{asynchronous} communication (cf. Remark~\ref{rem:asynch}) and 
extending our event-based approach 
to choreographic protocols; the framework in~\cite{CDV14} may provide a good starting point.
%via multiparty session types~\cite{DBLP:conf/popl/HondaYC08}. 
%We expect that well-formed systems would play a key role in defining the endpoint projections of choreographies described by (global) types.
%SEE JOURNAL FOR DISCISSION ON ADAPTATION FOR SESSION TYPES

\paragraph{\textbf{Acknowledgments.}} 
%\noindent{\textbf{Acknowledgments.}} 
We are grateful to 
Ilaria Castellani, 
Mariangiola Dezani-Ciancaglini, 
%M. Dezani, 
and 
the anonymous reviewers for useful remarks.
%The research reported in this paper 
This research was partially supported 
by %a Short-Term Scientific Mission 
%STSM
%grant to Di Giusto from 
COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems.
%(BETTY) -- \url{http://www.behavioural-types.eu}.

%\vspace{-2mm}

{\small
\bibliographystyle{abbrv}
\bibliography{referen}
}

\input{appendix}

\end{document}

